P:(UnitProp). Dec(P())  Dec(x:Unit. P(x)) 

latex

Definitions	i  j < k, P & Q, A, False, AB, , Surj(A; B; f), {i..j}, x:A. B(x), , Prop, x. t(x), P  Q, t  T, x:A. B(x), Unit, Dec(P), x(s), finite-type(T)
Lemmas	unit wf, decidable-exists-finite, it wf, decidable wf, surject wf, int seg wf, le wf